qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
↳ QTRS
↳ Overlay + Local Confluence
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QSORT(xs) → QS(half(length(xs)), xs)
QSORT(xs) → HALF(length(xs))
QSORT(xs) → LENGTH(xs)
QS(n, cons(x, xs)) → APPEND(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → HALF(n)
QS(n, cons(x, xs)) → FILTERLOW(get(n, cons(x, xs)), cons(x, xs))
QS(n, cons(x, xs)) → GET(n, cons(x, xs))
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → FILTERHIGH(get(n, cons(x, xs)), cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
LENGTH(cons(x, xs)) → LENGTH(xs)
HALF(s(s(x))) → HALF(x)
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
QSORT(xs) → QS(half(length(xs)), xs)
QSORT(xs) → HALF(length(xs))
QSORT(xs) → LENGTH(xs)
QS(n, cons(x, xs)) → APPEND(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → HALF(n)
QS(n, cons(x, xs)) → FILTERLOW(get(n, cons(x, xs)), cons(x, xs))
QS(n, cons(x, xs)) → GET(n, cons(x, xs))
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → FILTERHIGH(get(n, cons(x, xs)), cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
LENGTH(cons(x, xs)) → LENGTH(xs)
HALF(s(s(x))) → HALF(x)
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
HALF(s(s(x))) → HALF(x)
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
HALF(s(s(x))) → HALF(x)
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
HALF(s(s(x))) → HALF(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LENGTH(cons(x, xs)) → LENGTH(xs)
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LENGTH(cons(x, xs)) → LENGTH(xs)
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LENGTH(cons(x, xs)) → LENGTH(xs)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(n, cons(x, xs)) → QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
QS(n, cons(x, xs)) → QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
Used ordering: Polynomial interpretation [POLO]:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
POL(0) = 1
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = x1 + x2
POL(false) = 0
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 0
POL(get(x1, x2)) = 0
POL(half(x1)) = 0
POL(if1(x1, x2, x3, x4)) = x3 + x4
POL(if2(x1, x2, x3, x4)) = x3 + x4
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = 0
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
filterlow(n, nil) → nil
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
filterhigh(n, nil) → nil
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The value of delta used in the strict ordering is 3/4.
POL(if2(x1, x2, x3, x4)) = (13/4)x3
POL(get(x1, x2)) = 3/2 + (4)x1 + x2
POL(true) = 0
POL(filterhigh(x1, x2)) = 7/2 + (3/4)x1
POL(0) = 0
POL(cons(x1, x2)) = 0
POL(half(x1)) = (1/4)x1
POL(false) = 0
POL(filterlow(x1, x2)) = 9/4 + (15/4)x1 + x2
POL(s(x1)) = 4 + (4)x1
POL(QS(x1, x2)) = (1/4)x1
POL(if1(x1, x2, x3, x4)) = (1/4)x1
POL(ge(x1, x2)) = 4
POL(nil) = 0
half(s(s(x))) → s(half(x))
half(0) → 0
half(s(0)) → 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
POL(0) = 0
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false) = 0
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(half(x1)) = 0
POL(if1(x1, x2, x3, x4)) = 1 + x4
POL(if2(x1, x2, x3, x4)) = 1 + x4
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = 1
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ QTRS
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
POL(0) = 0
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false) = 0
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 0
POL(half(x1)) = 0
POL(if1(x1, x2, x3, x4)) = 1 + x4
POL(if2(x1, x2, x3, x4)) = 1 + x4
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QTRS
↳ QTRS
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QTRS
↳ QTRS
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ QTRS
↳ QTRS
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
POL(0) = 1
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false) = 1
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(half(x1)) = x1
POL(if1(x1, x2, x3, x4)) = x1 + x4
POL(nil) = 1
POL(s(x1)) = 1
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QTRS
↳ QTRS
↳ QTRS
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QTRS
↳ QTRS
↳ QTRS
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
half(0)
half(s(0))
half(s(s(x0)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ QTRS
↳ QTRS
↳ QTRS
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
POL(0) = 1
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false) = 1
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1 + x1
POL(if1(x1, x2, x3, x4)) = 1 + x4
POL(nil) = 0
POL(s(x1)) = x1
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ PisEmptyProof
↳ QTRS
↳ QTRS
↳ QTRS
↳ QTRS
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRS
↳ QTRS
if1'(true, n6, x12, xs4) → true
filterlow'(n11, cons(x19, xs8)) → if1'(ge(n11, x19), n11, x19, xs8)
if1'(false, n16, x26, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge(x', 0) → true
ge(s(x5), s(y'')) → ge(x5, y'')
if1(true, n6, x12, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x19, xs8)) → if1(ge(n11, x19), n11, x19, xs8)
if1(false, n16, x26, xs12) → cons(x26, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x39)) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
if1'(true, n6, x12, xs4) → true
filterlow'(n11, cons(x19, xs8)) → if1'(ge(n11, x19), n11, x19, xs8)
if1'(false, n16, x26, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge(x', 0) → true
ge(s(x5), s(y'')) → ge(x5, y'')
if1(true, n6, x12, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x19, xs8)) → if1(ge(n11, x19), n11, x19, xs8)
if1(false, n16, x26, xs12) → cons(x26, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x39)) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
[if1'4, filterlow'2] > [ge2, if14, filterlow2] > [true, false, nil] > cons2
equalbool2 > [true, false, nil] > cons2
not1 > [true, false, nil] > cons2
isafalse1 > [true, false, nil] > cons2
equalsort[a0]2 > [true, false, nil] > cons2
equalsort[a5]2 > and2 > [true, false, nil] > cons2
equalsort[a39]2 > [true, false, nil] > cons2
if1'4: [2,4,3,1]
true: multiset
or2: [2,1]
and2: multiset
filterlow'2: [1,2]
0: multiset
equalbool2: [2,1]
equalsort[a0]2: multiset
equalsort[a39]2: [2,1]
cons2: multiset
equalsort[a5]2: multiset
not1: multiset
witnesssort[a39]: multiset
isafalse1: multiset
false: multiset
filterlow2: [2,1]
s1: multiset
ge2: [2,1]
nil: multiset
if14: [4,2,3,1]
isatrue1: [1]
if1'(true, n6, x12, xs4) → true
filterlow'(n11, cons(x19, xs8)) → if1'(ge(n11, x19), n11, x19, xs8)
if1'(false, n16, x26, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge(x', 0) → true
ge(s(x5), s(y'')) → ge(x5, y'')
if1(true, n6, x12, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x19, xs8)) → if1(ge(n11, x19), n11, x19, xs8)
if1(false, n16, x26, xs12) → cons(x26, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x39)) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof
↳ QTRS
↳ QTRS
↳ QTRS
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRS
ge'(x', 0) → true
ge'(s(x6), s(y'')) → ge'(x6, y'')
if1'(true, n6, x14, xs4) → filterlow'(n6, xs4)
filterlow'(n11, cons(x22, xs8)) → or(if1'(ge(n11, x22), n11, x22, xs8), ge'(n11, x22))
if1'(false, n16, x30, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge'(0, s(x45)) → false
ge(x', 0) → true
ge(s(x6), s(y'')) → ge(x6, y'')
if1(true, n6, x14, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x22, xs8)) → if1(ge(n11, x22), n11, x22, xs8)
if1(false, n16, x30, xs12) → cons(x30, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x45)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x67))) → s(half(x67))
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a44](witness_sort[a44], witness_sort[a44]) → true
ge'(x', 0) → true
ge'(s(x6), s(y'')) → ge'(x6, y'')
if1'(true, n6, x14, xs4) → filterlow'(n6, xs4)
filterlow'(n11, cons(x22, xs8)) → or(if1'(ge(n11, x22), n11, x22, xs8), ge'(n11, x22))
if1'(false, n16, x30, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge'(0, s(x45)) → false
ge(x', 0) → true
ge(s(x6), s(y'')) → ge(x6, y'')
if1(true, n6, x14, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x22, xs8)) → if1(ge(n11, x22), n11, x22, xs8)
if1(false, n16, x30, xs12) → cons(x30, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x45)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x67))) → s(half(x67))
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a44](witness_sort[a44], witness_sort[a44]) → true
[ge'2, if1'4, filterlow'2, ge2, if14, filterlow2] > [cons2, or2, false, isafalse1] > [true, equalsort[a5]2] > and2
[ge'2, if1'4, filterlow'2, ge2, if14, filterlow2] > nil
half1 > 0
not1 > [cons2, or2, false, isafalse1] > [true, equalsort[a5]2] > and2
equalsort[a0]2 > [cons2, or2, false, isafalse1] > [true, equalsort[a5]2] > and2
witnesssort[a44] > [true, equalsort[a5]2] > and2
ge'2: [1,2]
true: multiset
if1'4: [2,4,1,3]
or2: [2,1]
and2: [2,1]
filterlow'2: [1,2]
0: multiset
equalsort[a44]2: multiset
witnesssort[a44]: multiset
equalbool2: multiset
equalsort[a0]2: [1,2]
cons2: multiset
equalsort[a5]2: [2,1]
half1: [1]
not1: [1]
isafalse1: multiset
false: multiset
filterlow2: [1,2]
ge2: [1,2]
nil: multiset
if14: [2,4,3,1]
isatrue1: [1]
ge'(x', 0) → true
if1'(true, n6, x14, xs4) → filterlow'(n6, xs4)
filterlow'(n11, cons(x22, xs8)) → or(if1'(ge(n11, x22), n11, x22, xs8), ge'(n11, x22))
if1'(false, n16, x30, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge'(0, s(x45)) → false
ge(x', 0) → true
if1(true, n6, x14, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x22, xs8)) → if1(ge(n11, x22), n11, x22, xs8)
if1(false, n16, x30, xs12) → cons(x30, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x45)) → false
half(0) → 0
half(s(0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a44](witness_sort[a44], witness_sort[a44]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRS
ge'(s(x6), s(y'')) → ge'(x6, y'')
ge(s(x6), s(y'')) → ge(x6, y'')
half(s(s(x67))) → s(half(x67))
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
ge'(s(x6), s(y'')) → ge'(x6, y'')
ge(s(x6), s(y'')) → ge(x6, y'')
half(s(s(x67))) → s(half(x67))
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
ge2 > ge'2
half1 > [s1, equalsort[a0]2] > ge'2
ge'2: [2,1]
half1: [1]
s1: multiset
ge2: [1,2]
equalsort[a0]2: multiset
ge'(s(x6), s(y'')) → ge'(x6, y'')
ge(s(x6), s(y'')) → ge(x6, y'')
half(s(s(x67))) → s(half(x67))
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ QTRS
↳ QTRS
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
if2'(true, n82, x105, xs61) → true
filterhigh'(n91, cons(x116, xs68)) → if2'(ge(x116, n91), n91, x116, xs68)
if2'(false, n100, x127, xs75) → filterhigh'(n100, xs75)
filterhigh'(n109, nil) → false
ge(x', 0) → true
ge(s(x9), s(y'')) → ge(x9, y'')
if1(true, n14, x20, xs10) → filterlow(n14, xs10)
filterlow(n23, cons(x31, xs17)) → if1(ge(n23, x31), n23, x31, xs17)
if1(false, n32, x42, xs24) → cons(x42, filterlow(n32, xs24))
filterlow(n41, nil) → nil
ge(0, s(x63)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x94))) → s(half(x94))
if2(true, n82, x105, xs61) → filterhigh(n82, xs61)
filterhigh(n91, cons(x116, xs68)) → if2(ge(x116, n91), n91, x116, xs68)
if2(false, n100, x127, xs75) → cons(x127, filterhigh(n100, xs75))
filterhigh(n109, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
if2'(true, n82, x105, xs61) → true
filterhigh'(n91, cons(x116, xs68)) → if2'(ge(x116, n91), n91, x116, xs68)
if2'(false, n100, x127, xs75) → filterhigh'(n100, xs75)
filterhigh'(n109, nil) → false
ge(x', 0) → true
ge(s(x9), s(y'')) → ge(x9, y'')
if1(true, n14, x20, xs10) → filterlow(n14, xs10)
filterlow(n23, cons(x31, xs17)) → if1(ge(n23, x31), n23, x31, xs17)
if1(false, n32, x42, xs24) → cons(x42, filterlow(n32, xs24))
filterlow(n41, nil) → nil
ge(0, s(x63)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x94))) → s(half(x94))
if2(true, n82, x105, xs61) → filterhigh(n82, xs61)
filterhigh(n91, cons(x116, xs68)) → if2(ge(x116, n91), n91, x116, xs68)
if2(false, n100, x127, xs75) → cons(x127, filterhigh(n100, xs75))
filterhigh(n109, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
[if2'4, filterhigh'2] > [ge2, if14, filterlow2] > [true, cons2, false, nil, 0, isatrue1, equalsort[a65]2, witnesssort[a65]] > and2
[if24, filterhigh2] > [ge2, if14, filterlow2] > [true, cons2, false, nil, 0, isatrue1, equalsort[a65]2, witnesssort[a65]] > and2
or2 > [true, cons2, false, nil, 0, isatrue1, equalsort[a65]2, witnesssort[a65]] > and2
equalsort[a0]2 > [true, cons2, false, nil, 0, isatrue1, equalsort[a65]2, witnesssort[a65]] > and2
equalsort[a5]2 > [true, cons2, false, nil, 0, isatrue1, equalsort[a65]2, witnesssort[a65]] > and2
if24: [4,2,1,3]
true: multiset
filterhigh'2: [1,2]
filterhigh2: [2,1]
or2: multiset
and2: multiset
if2'4: [2,4,1,3]
0: multiset
equalbool2: multiset
equalsort[a0]2: [1,2]
cons2: multiset
equalsort[a5]2: multiset
half1: [1]
equalsort[a65]2: multiset
not1: multiset
false: multiset
filterlow2: [1,2]
witnesssort[a65]: multiset
ge2: [1,2]
nil: multiset
if14: [2,4,1,3]
isatrue1: multiset
if2'(true, n82, x105, xs61) → true
filterhigh'(n91, cons(x116, xs68)) → if2'(ge(x116, n91), n91, x116, xs68)
if2'(false, n100, x127, xs75) → filterhigh'(n100, xs75)
filterhigh'(n109, nil) → false
ge(x', 0) → true
if1(true, n14, x20, xs10) → filterlow(n14, xs10)
filterlow(n23, cons(x31, xs17)) → if1(ge(n23, x31), n23, x31, xs17)
if1(false, n32, x42, xs24) → cons(x42, filterlow(n32, xs24))
filterlow(n41, nil) → nil
ge(0, s(x63)) → false
half(0) → 0
half(s(0)) → 0
if2(true, n82, x105, xs61) → filterhigh(n82, xs61)
filterhigh(n91, cons(x116, xs68)) → if2(ge(x116, n91), n91, x116, xs68)
if2(false, n100, x127, xs75) → cons(x127, filterhigh(n100, xs75))
filterhigh(n109, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
ge(s(x9), s(y'')) → ge(x9, y'')
half(s(s(x94))) → s(half(x94))
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
ge(s(x9), s(y'')) → ge(x9, y'')
half(s(s(x94))) → s(half(x94))
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 2
POL(ge(x1, x2)) = 2·x1 + x2
POL(half(x1)) = 2 + 2·x1
POL(isa_false(x1)) = 2 + 2·x1
POL(s(x1)) = 1 + 2·x1
POL(true) = 1
ge(s(x9), s(y'')) → ge(x9, y'')
half(s(s(x94))) → s(half(x94))
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof
↳ QTRS
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
if2'(true, n82, x105, xs61) → true
filterhigh'(n91, cons(x116, xs68)) → if2'(ge(x116, n91), n91, x116, xs68)
if2'(false, n100, x127, xs75) → filterhigh'(n100, xs75)
filterhigh'(n109, nil) → false
ge(x', 0) → true
ge(s(x9), s(y'')) → ge(x9, y'')
if1(true, n14, x20, xs10) → filterlow(n14, xs10)
filterlow(n23, cons(x31, xs17)) → if1(ge(n23, x31), n23, x31, xs17)
if1(false, n32, x42, xs24) → cons(x42, filterlow(n32, xs24))
filterlow(n41, nil) → nil
ge(0, s(x63)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x94))) → s(half(x94))
if2(true, n82, x105, xs61) → filterhigh(n82, xs61)
filterhigh(n91, cons(x116, xs68)) → if2(ge(x116, n91), n91, x116, xs68)
if2(false, n100, x127, xs75) → cons(x127, filterhigh(n100, xs75))
filterhigh(n109, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a67](witness_sort[a67], witness_sort[a67]) → true
if2'(true, n82, x105, xs61) → true
filterhigh'(n91, cons(x116, xs68)) → if2'(ge(x116, n91), n91, x116, xs68)
if2'(false, n100, x127, xs75) → filterhigh'(n100, xs75)
filterhigh'(n109, nil) → false
ge(x', 0) → true
ge(s(x9), s(y'')) → ge(x9, y'')
if1(true, n14, x20, xs10) → filterlow(n14, xs10)
filterlow(n23, cons(x31, xs17)) → if1(ge(n23, x31), n23, x31, xs17)
if1(false, n32, x42, xs24) → cons(x42, filterlow(n32, xs24))
filterlow(n41, nil) → nil
ge(0, s(x63)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x94))) → s(half(x94))
if2(true, n82, x105, xs61) → filterhigh(n82, xs61)
filterhigh(n91, cons(x116, xs68)) → if2(ge(x116, n91), n91, x116, xs68)
if2(false, n100, x127, xs75) → cons(x127, filterhigh(n100, xs75))
filterhigh(n109, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a67](witness_sort[a67], witness_sort[a67]) → true
[if2'4, filterhigh'2] > [ge2, if14, filterlow2] > [true, cons2, false, nil, 0, isatrue1, equalsort[a67]2, witnesssort[a67]] > and2
[if24, filterhigh2] > [ge2, if14, filterlow2] > [true, cons2, false, nil, 0, isatrue1, equalsort[a67]2, witnesssort[a67]] > and2
or2 > [true, cons2, false, nil, 0, isatrue1, equalsort[a67]2, witnesssort[a67]] > and2
equalsort[a0]2 > [true, cons2, false, nil, 0, isatrue1, equalsort[a67]2, witnesssort[a67]] > and2
equalsort[a5]2 > [true, cons2, false, nil, 0, isatrue1, equalsort[a67]2, witnesssort[a67]] > and2
if24: [4,2,1,3]
true: multiset
filterhigh'2: [1,2]
filterhigh2: [2,1]
or2: multiset
and2: multiset
if2'4: [2,4,1,3]
0: multiset
equalbool2: multiset
equalsort[a0]2: [1,2]
cons2: multiset
equalsort[a5]2: multiset
half1: [1]
witnesssort[a67]: multiset
not1: multiset
false: multiset
filterlow2: [1,2]
equalsort[a67]2: multiset
ge2: [1,2]
nil: multiset
if14: [2,4,1,3]
isatrue1: multiset
if2'(true, n82, x105, xs61) → true
filterhigh'(n91, cons(x116, xs68)) → if2'(ge(x116, n91), n91, x116, xs68)
if2'(false, n100, x127, xs75) → filterhigh'(n100, xs75)
filterhigh'(n109, nil) → false
ge(x', 0) → true
if1(true, n14, x20, xs10) → filterlow(n14, xs10)
filterlow(n23, cons(x31, xs17)) → if1(ge(n23, x31), n23, x31, xs17)
if1(false, n32, x42, xs24) → cons(x42, filterlow(n32, xs24))
filterlow(n41, nil) → nil
ge(0, s(x63)) → false
half(0) → 0
half(s(0)) → 0
if2(true, n82, x105, xs61) → filterhigh(n82, xs61)
filterhigh(n91, cons(x116, xs68)) → if2(ge(x116, n91), n91, x116, xs68)
if2(false, n100, x127, xs75) → cons(x127, filterhigh(n100, xs75))
filterhigh(n109, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a67](witness_sort[a67], witness_sort[a67]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
ge(s(x9), s(y'')) → ge(x9, y'')
half(s(s(x94))) → s(half(x94))
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
ge(s(x9), s(y'')) → ge(x9, y'')
half(s(s(x94))) → s(half(x94))
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 2
POL(ge(x1, x2)) = 2·x1 + x2
POL(half(x1)) = 2 + 2·x1
POL(isa_false(x1)) = 2 + 2·x1
POL(s(x1)) = 1 + 2·x1
POL(true) = 1
ge(s(x9), s(y'')) → ge(x9, y'')
half(s(s(x94))) → s(half(x94))
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof